$\forall$$e$$<$${\it e'}$.$P$($e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$e$:es{-}E(${\it es}$). es{-}locl(${\it es}$; $e$; ${\it e'}$) $\Rightarrow$ $P$($e$)